﻿using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using TSU.FAMC.ComputerEngineering.Classes.Bdds.Basis;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Functions;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Fundamental;
using TSU.FAMC.ComputerEngineering.Classes.Enums;

namespace TSU.FAMC.ComputerEngineering.Classes.Bdds
{
    /// <summary>
    /// Ordered bdd.
    /// </summary>
    public class OrderedBdd: BaseBdd, ICloneable
    {
        /// <summary>
        /// Order of input variables in bdd.
        /// </summary>
        public List<string> Order = new List<string>();

        /// <summary>
        /// Checkes whether obdd order is valid by rounding graph.
        /// </summary>
        /// <returns>True if order is right against obdd structure.</returns>
        public bool ValidateOrder()
        {
            return Order.Count != 0 && Roots.All(DoValidateOrder);
        }

        /// <summary>
        /// Validates bdd structure against variables order by rounded graph.
        /// </summary>
        /// <param name="currentNode">Currently rounding node.</param>
        /// <returns>True if order is valid.</returns>
        private bool DoValidateOrder(Node currentNode)
        {
            if (Sinks.Contains(currentNode))
            {
                // terminal node
                return true;
            }

            if (!Order.Contains(currentNode.Label))
            {
                return false;
            }

            var children = currentNode.Children.Select(edge => edge.Child).ToList();
            foreach (var child in children.Where(child => !Sinks.Contains(child)))
            {
                if (Order.IndexOf(child.Label) <= Order.IndexOf(currentNode.Label))
                {
                    return false;
                }

                if (!DoValidateOrder(child))
                {
                    return false;
                }
            }

            return true;
        }

        /// <summary>
        /// Validate structure of ordered bdd. It's a compute-intensive operation.
        /// </summary>
        /// <returns>True if bdd structure is ok.</returns>
        public override bool ValidateStructure()
        {
            return base.ValidateStructure() && ValidateOrder();
        }

        /// <summary>
        /// Searches for all paths to 1-terminal node and presents them as BooleanSystem object.
        /// </summary>
        /// <returns>Orthogonal Disjunctive Normal form retrieved from bdd as Boolean system.</returns>
        public BooleanSystem Odnf()
        {
            var terminal1 = Sinks.SingleOrDefault(s => s.IsTerminal1);
            if (terminal1 == null)
            {
                throw new InvalidDataException("No terminal-1 node found.");
            }

            // searching paths
            var paths = new List<List<PathElement>>();
            var labels = new List<string>();
            DoFindOneToRootPaths(terminal1, paths, labels);

            // examining labels and determining system variables dimension.
            var dimension = Order.Count;

            // ordering paths by roots
            if (Roots.Count > 1)
            {
                paths.Sort(
                    (p1, p2) =>
                    Roots.IndexOf(p1.Last().Node) == Roots.IndexOf(p2.Last().Node)
                        ? 0
                        : Roots.IndexOf(p1.Last().Node) < Roots.IndexOf(p2.Last().Node) ? -1 : 1);
            }

            // processing paths
            Node lastRoot = null;
            var system = new BooleanSystem();
            foreach (var path in paths)
            {
                if (!ReferenceEquals(path.Last().Node, lastRoot))
                {
                    // new function started
                    var function = new BooleanFunction();
                    system.Functions.Add(function);
                    lastRoot = path.Last().Node;
                }

                var cube = new Cube(dimension);
                for (var i = 0; i < dimension; i++)
                {
                    cube[i] = BooleanValue.Undefined;
                }

                foreach (var pathElement in path)
                {
                    var index = Order.IndexOf(pathElement.Node.Label);
                    cube[index] = pathElement.Sign;
                }
                system.Functions.Last().Domain1.Add(cube);
            }

            return system;
        }

        /// <summary>
        /// Searches for paths to the roots recursively to build ODNF.
        /// </summary>
        /// <param name="currentNode">Currently evaluated node of bdd.</param>
        /// <param name="paths">Root-to-1 found paths.</param>
        /// <param name="labels">List of all evaluated label values.</param>
        /// <param name="currentPath">Current bdd path.</param>
        private void DoFindOneToRootPaths(Node currentNode, List<List<PathElement>> paths, List<string> labels, List<PathElement> currentPath = null)
        {
            if (currentPath == null)
            {
                currentPath = new List<PathElement>();
            }

            if (!labels.Contains(currentNode.Label))
            {
                labels.Add(currentNode.Label);
            }

            if (Roots.Contains(currentNode))
            {
                // root reached
                var newPath = currentPath.ToList();
                paths.Add(newPath);

                return;
            }

            // going up
            foreach (var edge in currentNode.Parents)
            {
                var parent = edge.Parent;

                // incrementing path
                currentPath.Add(new PathElement { Node = parent, Sign = edge.Type == BddEdgeType.False ? BooleanValue.False : BooleanValue.True });

                DoFindOneToRootPaths(parent, paths, labels, currentPath);

                // decrementing path
                currentPath.RemoveAt(currentPath.Count - 1);
            }
        }

        /// <summary>
        /// Builds ordered bdd, representing conjunction.
        /// </summary>
        /// <param name="cube">Cube representation of conjunction.</param>
        /// <param name="order">Variables order.</param>
        /// <returns></returns>
        public static OrderedBdd BuildFromCube(Cube cube, List<string> order)
        {
            if (cube.Dimension != order.Count)
            {
                // incompatible cube and var order
                return null;
            }

            if (cube.Rank == 0)
            {
                return new OrderedBdd {Order = order};
            }

            // building terminal sinks
            var bdd = new OrderedBdd {Order = order};
            var sink0 = new Node {Label = "0"};
            var sink1 = new Node { Label = "1" };
            bdd.Sinks.Add(sink0);
            bdd.Sinks.Add(sink1);

            var lastNode = sink1;
            for (var i = order.Count - 1; i >= 0; i--)
            {
                var label = order[i];
                if (cube[i] == BooleanValue.Undefined)
                {
                    // unspecified variable
                    continue;
                }

                var node = new Node {Label = label};

                if (cube[i] == BooleanValue.False)
                {
                    node.LinkChildHigh(sink0);
                    node.LinkChildLow(lastNode);
                }
                else if (cube[i] == BooleanValue.True)
                {
                    node.LinkChildLow(sink0);
                    node.LinkChildHigh(lastNode);
                }

                lastNode = node;
            }

            bdd.Roots.Add(lastNode);
            return bdd;
        }


        /// <summary>
        /// Performs simplification operation on ordered bdd to build more compact equivalent bdd.
        /// </summary>
        public override void Optimize()
        {
            if (Order.Count == 0)
            {
                throw new InvalidOperationException("Input variable order required.");
            }

            // building bdd levels (n+1)
            var levels = new List<List<Node>>();
            for (var i = 0; i < Order.Count + 1; i++)
            {
                levels.Add(new List<Node>());
            }

            var visitedNodes = new List<Node>();
            foreach (var root in Roots)
            {
                DoBuildLevels(root, levels, visitedNodes);
            }


            // analyzing bdd
            var reducedBdd = visitedNodes.Select(t => new Node()).ToList();
            var uniqueTableLevel = new List<UniqueTableNode>();
            var nextId = -1;
            for (var i = Order.Count; i >= 0; i--)
            {
                var level = levels[i];
                uniqueTableLevel.Clear();

                foreach (var node in level)
                {
                    if (Sinks.Contains(node))
                    {
                        // terminal node
                        uniqueTableLevel.Add(new UniqueTableNode { KeyLow = Int32.Parse(node.Label), KeyHigh = Int32.Parse(node.Label), Node = node });
                        node.Id = Int32.Parse(node.Label);
                    }
                    else if (node.Low().Id == node.High().Id)
                    {
                        // redundant node
                        node.Id = node.Low().Id;

                        if (Roots.Contains(node))
                        {
                            // removing from roots
                            Roots.Remove(node);

                            // setting new root
                            var newRoot = reducedBdd[node.Low().Id];
                            Roots.Add(newRoot);
                        }

                        // unlinking children
                        foreach (var child in node.Children.Select(edge => edge.Child).ToList())
                        {
                            node.UnlinkNode(child);
                        }
                    }
                    else
                    {
                        uniqueTableLevel.Add(new UniqueTableNode { KeyLow = node.Low().Id, KeyHigh = node.High().Id, Node = node });
                    }
                }

                // sorting uniqueTableLevel
                uniqueTableLevel.Sort((obj1, obj2) => obj1.KeyLow == obj2.KeyLow ? 0 : obj1.KeyLow < obj2.KeyLow ? -1 : 1);

                var oldKey = new UniqueTableNode {KeyLow = -1, KeyHigh = -1};
                foreach (var tableNode in uniqueTableLevel)
                {
                    if (tableNode.KeyLow == oldKey.KeyLow && tableNode.KeyHigh == oldKey.KeyHigh)
                    {
                        // matches existing node
                        tableNode.Node.Id = nextId;

                        // unlinking children
                        foreach (var child in tableNode.Node.Children.Select(edge => edge.Child).ToList())
                        {
                            tableNode.Node.UnlinkNode(child);
                        }

                        // removing from sinks
                        if (Sinks.Contains(tableNode.Node))
                        {
                            Sinks.Remove(tableNode.Node);
                        }
                    }
                    else
                    {
                        // unique node
                        nextId = nextId + 1;
                        tableNode.Node.Id = nextId;
                        reducedBdd[nextId] = tableNode.Node;

                        if (!Sinks.Contains(tableNode.Node))
                        {
                            // linking childs for non-terminal node
                            var lowId = tableNode.Node.Low().Id;
                            if (!ReferenceEquals(tableNode.Node.Low(), reducedBdd[lowId]))
                            {
                                tableNode.Node.UnlinkNode(tableNode.Node.Low());
                                tableNode.Node.LinkChildLow(reducedBdd[lowId]);
                            }

                            var highId = tableNode.Node.High().Id;
                            if (!ReferenceEquals(tableNode.Node.High(), reducedBdd[highId]))
                            {
                                tableNode.Node.UnlinkNode(tableNode.Node.High());
                                tableNode.Node.LinkChildHigh(reducedBdd[highId]);
                            }
                        }

                        oldKey.KeyLow = tableNode.KeyLow;
                        oldKey.KeyHigh = tableNode.KeyHigh;
                    }
                }
            }
        }

        /// <summary>
        /// Builds bdd levels by rounding bdd.
        /// </summary>
        /// <param name="currentNode">Currently rounding node.</param>
        /// <param name="levels">Bdd levels.</param>
        /// <param name="visitedNodes">An array of already visited nodes.</param>
        private void DoBuildLevels(Node currentNode, List<List<Node>> levels, List<Node> visitedNodes)
        {
            if (visitedNodes.Contains(currentNode))
            {
                return;
            }

            var index = Order.IndexOf(currentNode.Label);
            if (currentNode.Children.Count == 0 && Sinks.Contains(currentNode))
            {
                index = Order.Count;
            }
            else if (index < 0)
            {
                // something wrong
                throw new InvalidDataException("The label of the currently rounding node does not satisfy obdd order.");
            }

            levels[index].Add(currentNode);
            visitedNodes.Add(currentNode);

            // rounding children
            var children = currentNode.Children.Select(edge => edge.Child);
            foreach (var child in children)
            {
                DoBuildLevels(child, levels, visitedNodes);
            }
        }

        /// <summary>
        /// Applies Or operation on two bdds.
        /// </summary>
        /// <param name="bdd">Bdd to use in operation.</param>
        public OrderedBdd Or(OrderedBdd bdd)
        {
            return Apply(bdd, BooleanOperation.Disjunction);
        }

        /// <summary>
        /// Applies And operation on two bdds.
        /// </summary>
        /// <param name="bdd">Bdd to use in operation.</param>
        public OrderedBdd And(OrderedBdd bdd)
        {
            return Apply(bdd, BooleanOperation.Conjucntion);
        }

        /// <summary>
        /// Applies boolean operation on bdds.
        /// </summary>
        /// <param name="bdd">Bdd to apply operation with.</param>
        /// <param name="operation">Boolean operation to apply.</param>
        /// <returns>Bdd as a result of operation.</returns>
        private OrderedBdd Apply(OrderedBdd bdd, BooleanOperation operation)
        {
            // checking roots
            if (!ValidateRoots())
            {
                throw new InvalidDataException("Invalid roots specified for main bdd.");
            }
            if (!bdd.ValidateRoots())
            {
                throw new InvalidDataException("Invalid roots specified for second bdd.");
            }

            // checking whether each bdd has only one root
            if (Roots.Count != 1 || bdd.Roots.Count != 1)
            {
                throw new InvalidDataException("Each bdd must have only one root.");
            }

            // checking sinks
            if (!ValidateSinks())
            {
                throw new InvalidDataException("Invalid sinks specified for main bdd.");
            }
            if (!bdd.ValidateSinks())
            {
                throw new InvalidDataException("Invalid sinks specified for second bdd.");
            }

            // checking whether all sinks has labels 0 or 1
            if (Sinks.Where(sink => sink.Label != "0" && sink.Label != "1").Any())
            {
                throw new InvalidDataException("Invalid sink label in main bdd.");
            }
            if (bdd.Sinks.Where(sink => sink.Label != "0" && sink.Label != "1").Any())
            {
                throw new InvalidDataException("Invalid sink label in second bdd.");
            }

            // checking whether orders are identical
            if (Order.Count != bdd.Order.Count ||
                Order.Where((t, i) => t != bdd.Order[i]).Any())
            {
                throw new InvalidDataException("Bdd orders are not compatible.");
            }

            // applying bdds
            var table = new ApplyTable();
            var resultBdd = new OrderedBdd { Order = Order };
            var resultRoot = DoApply(Roots.First(), bdd.Roots.First(), operation, table, resultBdd);
            resultBdd.Roots.Add(resultRoot);

            // reducing bdd
            resultBdd.Optimize();

            return resultBdd;
        }

        /// <summary>
        /// Apply boolean operation on two bdds recursively.
        /// </summary>
        /// <param name="v1">Current node of the first bdd.</param>
        /// <param name="v2">Current node of the second bdd.</param>
        /// <param name="op">Boolean operation.</param>
        /// <param name="t">Cache table of evaluated nodes.</param>
        /// <param name="resultBdd">Resulting bdd.</param>
        /// <returns>Result of boolean operation on two nodes.</returns>
        private Node DoApply(Node v1, Node v2, BooleanOperation op, ApplyTable t, BaseBdd resultBdd)
        {
            var resultNode = t[v1, v2];
            if (resultNode != null)
            {
                // have already evaluated
                return resultNode;
            }

            // creating new node of resulting bdd
            resultNode = new Node();
            t[v1, v2] = resultNode;


            // calculating operation result
            var opResult = BooleanValue.Undefined;

            if (op == BooleanOperation.Disjunction)
            {
                if (v1.Children.Count == 0 && v1.Label == "1" || 
                    v2.Children.Count == 0 && v2.Label == "1")
                {
                    opResult = BooleanValue.True;
                }
                else if (v1.Children.Count == 0 && v2.Children.Count == 0)
                {
                    // terminal-0 nodes
                    opResult = BooleanValue.False;
                }
                else
                {
                    // one or both nodes are non-terminal
                    opResult = BooleanValue.Undefined;
                }
            }
            else if (op == BooleanOperation.Conjucntion)
            {
                if (v1.Children.Count == 0 && v1.Label == "0" ||
                    v2.Children.Count == 0 && v2.Label == "0")
                {
                    opResult = BooleanValue.False;
                }
                else if (v1.Children.Count == 0 && v2.Children.Count == 0)
                {
                    // terminal-1 nodes
                    opResult = BooleanValue.True;
                }
                else
                {
                    // one or both nodes are non-terminal
                    opResult = BooleanValue.Undefined;
                }
            }


            if (opResult != BooleanValue.Undefined)
            {
                // creating terminal node
                resultNode.Label = opResult == BooleanValue.False ? "0" : "1";
                resultBdd.Sinks.Add(resultNode);
            }
            else
            {
                // non-terminal node
                var v1Index = v1.Children.Count == 0 ? Order.Count : Order.IndexOf(v1.Label);
                var v2Index = v2.Children.Count == 0 ? Order.Count : Order.IndexOf(v2.Label);
                if (v1Index < 0 || v2Index < 0)
                {
                    throw new InvalidDataException("Bdd orders are not compatible.");
                }

                resultNode.Label = v1Index < v2Index ? v1.Label : v2.Label;
                
                Node vlow1;
                Node vlow2;
                Node vhigh1;
                Node vhigh2;

                if (resultNode.Label == v1.Label)
                {
                    vlow1 = v1.Low();
                    vhigh1 = v1.High();
                }
                else
                {
                    vlow1 = v1;
                    vhigh1 = v1;
                }

                if (resultNode.Label == v2.Label)
                {
                    vlow2 = v2.Low();   
                    vhigh2 = v2.High();
                }
                else
                {
                    vlow2 = v2;
                    vhigh2 = v2;
                }

                resultNode.LinkChildLow(DoApply(vlow1, vlow2, op, t, resultBdd));
                resultNode.LinkChildHigh(DoApply(vhigh1, vhigh2, op, t, resultBdd));
            }

            return resultNode;
        }

        /// <summary>
        /// Clones itself.
        /// </summary>
        /// <returns>Copy of itself.</returns>
        public object Clone()
        {
            return Or(this);
        }
    }

    /// <summary>
    /// Auxiliary data structure for Optimize method.
    /// </summary>
    class UniqueTableNode
    {
        public int KeyLow;
        public int KeyHigh;
        public Node Node;
    }

    /// <summary>
    /// Auxiliary class for Apply method.
    /// </summary>
    class ApplyTable
    {
        private readonly Dictionary<KeyValuePair<Node, Node>, Node> _table = new Dictionary<KeyValuePair<Node, Node>, Node>();

        public Node this[Node node1, Node node2]
        {
            get
            {
                var records =
                    _table.Where(rec => ReferenceEquals(rec.Key.Key, node1) && ReferenceEquals(rec.Key.Value, node2));

                if (records.Count() == 0)
                {
                    return null;
                }

                return records.First().Value;
            }

            set
            {
                var records =
                    _table.Where(rec => ReferenceEquals(rec.Key.Key, node1) && ReferenceEquals(rec.Key.Value, node2));

                if (records.Count() > 0 && !ReferenceEquals(records.First().Value, null))
                {
                    // key exists

                    if (ReferenceEquals(records.First().Value, value))
                    {
                        // record already exists
                        return;
                    }

                    // updating record
                    _table.Remove(records.First().Key);
                    _table.Add(new KeyValuePair<Node, Node>(node1, node2), value);
                    return;
                }

                // creating record
                _table.Add(new KeyValuePair<Node, Node> (node1, node2), value);
            }
        }
    }
}
